Ví dụ Luận lý Hoare

Example 1
{ x + 1 = 43 } {\displaystyle \{x+1=43\}\!}   y := x + 1   {\displaystyle \ y:=x+1\ \!} { y = 43 } {\displaystyle \{y=43\}\!} (Tiên đề gán)
( x + 1 = 43 ⟹ x = 42 ) {\displaystyle (x+1=43\implies x=42)}
{ x = 42 } {\displaystyle \{x=42\}\!}   y := x + 1   {\displaystyle \ y:=x+1\ \!} { y = 43 ∧ x = 42 } {\displaystyle \{y=43\land x=42\}\!} (Luật hệ quả)
Example 2
{ x + 1 ≤ N } {\displaystyle \{x+1\leq N\}\!}   x := x + 1   {\displaystyle \ x:=x+1\ \!} { x ≤ N }   {\displaystyle \{x\leq N\}\ \!} (Tiên đề gán)
( x < N ⟹ x + 1 ≤ N {\displaystyle x<N\implies x+1\leq N} với x, N là kiểu số nguyên.)
{ x < N } {\displaystyle \{x<N\}\!}   x := x + 1   {\displaystyle \ x:=x+1\ \!} { x ≤ N }   {\displaystyle \{x\leq N\}\ \!} (Luật hệ quả)